作者：Sebastián Urciuoli
我们为一阶语法中lambda演算的形式元理论提供了一个框架，有两种名称，一种表示自由变量和绑定变量，另一种表示常量，并使用Stoughton的多次替换。在该框架的基础上，我们形式化了简单类型lambda演算和系统T的强归一化定理的Girard证明。对于后者，我们还对原始证明进行了简化。整个开发已经使用Agda系统进行了机器检查。
We present a framework for the formal meta-theory of lambda calculi in first-order syntax, with two sorts of names, one to represent both free and bound variables, and the other for constants, and by using Stoughton’s multiple substitutions. On top of the framework we formalize Girard’s proof of the Strong Normalization Theorem for both the simply-typed lambda calculus and System T. As to the latter, we also present a simplification of the original proof. The whole development has been machine-checked using the Agda system.
论文链接：http://arxiv.org/pdf/2303.13258v1
更多计算机论文：http://cspaper.cn/